package ch.epfl.lara.matcheck.verify.provers.formdecider;

import ch.epfl.lara.matcheck.ast._

object FormDeciderStringer extends FormulaStringer {self: FormulaStringer =>
  
  override def apply(formula: Formula) = asString(formula)
  

  override protected def asString(formula: Formula): String = formula match {
    case And(left,right) => "((" + asString(left) + ") & (" + asString(right) + "))" 
      
    case Or(left,right) =>  "((" + asString(left) + ") | (" + asString(right) + "))"
      
    case Imply(left,right) => "(" + asString(left) + " --> " + asString(right) + ")"
      
    case Neg(f) => "~(" + asString(f) + ")"
      
    case Equality(e,f) => "(" + asString(e) + " = " + asString(f) + ")" 
    
    case SetComprehension(x,f) => "{" + x + ". " + asString(f) + "}"
      
    case SubsetEq(left,right) =>  "(" + asString(left)  + " \\<subseteq>  "  + asString(right) + ")" 
      
    case EqSet(left,right) => "(" + asString(left) + " = " + asString(right) + ")"
    
    case In(x,Set("BType")) =>  "(" + asString(x) + ")"
    case In(x,Set("IType")) =>  "(" + "("+asString(x) +"::int) : (IType :: int set)" + ")"
    case In(x,set) =>  "(" + asString(x) + " : " + asString(set) + ")"
    
    case Forall(x,form) => "(ALL " + x + ". " + asString(form) + ")" 
      
    case Tru => "true"
      
    case Flse => "false"
    
    case Function(name,elems) => name + elems.map(asString(_)).mkString("(",",",")")
    
    case Deref(obj,field) => 
      System.err.print("\nerror: ")
      ch.epfl.lara.matcheck.util.printer.PrettyPrinterFormula(formula)
      error("this expression need to be desugared")
      
    case Element(name) => name
    
    case StringLit0(str) => "string__" + str 
 
    case Set(name) => name
    
    case EmptySet => "{}"
      
    case Union(left,right) => "(" + asString(left) + " Un " + asString(right) + ")"
    
    case Intersection(left,right) => "(" + asString(left) + " Int " + asString(right) + ")"
    
    case Eq(left,right) => "(" + asString(left) + " = " + asString(right) + ")"
    
    case NotEq(left,right) => "~(" + asString(left) + " = " + asString(right) + ")"
      
    case Less(left,right) => "(" + asString(left) + " < " + asString(right) + ")" 
    
    case LessEq(left,right) => "(" + asString(left) + " <= " + asString(right) + ")"
    
    case Const(n) => n + ""
      
    case Plus(left,right) => "(" + asString(left) + " + " + asString(right) + ")"
    
    case Minus(left,right) => "(" + asString(left) + " - " + asString(right) + ")"
    
    case Div(left,right) => "(" + asString(left) + " / " + asString(right) + ")"
    
    case Prod(left,right) => "(" + asString(left) + " * " + asString(right) + ")"
    
    case Mod(left,right) => "(" + asString(left) + " mod " + asString(right) + ")"
   
    //Internally used
    //case Equality(left,right) => "(" + asString(left) + " = " + asString(right) + ")"
      
    case IntVar(x) => x
  }
 
}
